报告题目：基于广义可能性测度的计算树逻辑模型检测

报告人：李永明教授（陕西师范大学，博士生导师）

时间：2015-6-2 16：00

地点：数学实验室

摘要：信息系统的功能正确性验证和性能可满足性验证是信息系统可信性的重要方面。模型检测是一种很重要的自动化验证技术，是形式化验证的一种主要研究方向，而量化模型检测是当前模型检测技术的一种主要研究分支，形成信息系统的功能正确性验证和性能可满足性验证的主要方法之一。本报告将主要讲述新近提出的基于可能性测度的模型检测方法—基于广义可能性测度的计算树逻辑(CTL)模型检测，它是和概率模型检测互补的一种模型检测方法。我们提出了基于广义可能性测度的CTL模型检测方法：模型用广义可能性Kripke结构表示，性质用广义可能性计算树逻辑（CTL）表示，证明了广义可能性CTL在表达能力方面强于经典CTL，模型检测算法采用矩阵运算，其具有多项式时间复杂性。

附.李永明简介:

    李永明，1966年3月生，陕西省大荔县人，教授（陕西师范大学二级教授），博士生导师。

    主要研究方向：非经典计算理论、定量模型检测、计算智能、模糊系统分析、量子信息学、格上拓扑学。

    2001年国务院政府特殊津贴获得者，2002教育部第三届“高校青年教师奖”（教育部高层次人才奖励计划），陕西省三秦人才津贴获得者。目前担任陕西师范大学图书馆馆长。担任国际IEEE计算智能模糊系统技术委员会委员，中国系统工程学会模糊数学与模糊系统委员会副主任委员，全国运筹学会智能计算学会副理事长，全国高等师范学校计算机教育委员会副理事长。在科学出版社出版专著《模糊系统分析》一部，在国内外著名杂志发表论文200余篇，其中《SCI》源期刊论文90余篇。

    承担973项目子课题、国家自然科学基金、教育部高等学校博士点基金、教育部优秀青年教师教学科研奖励计划、教育部留学人员启动经费等项目10余项。曾获得省部级科学技术奖4项。

汕头大学理学院

2015年6月2日